import java.io.BufferedReader;
import java.io.DataInputStream;
import java.io.FileInputStream;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.Scanner;

public class InferenceSearcher {
	static ArrayList<String> KB = new ArrayList<String>();
	static ArrayList<String> exhausted = new ArrayList<String>();
	static int depth = 0;
	static String assertion = "";
	
	public static void main(String args[]) {
		Scanner input = new Scanner(System.in);
		String file = "";
		
		// Get user input
		System.out.println("Please enter file name");
		file = input.next();	
		System.out.println("Please enter assertion to be proved:");
		assertion = input.next();
		
		// Initialize search
		initialize(file, assertion);
		
		
	}
	
	private static void initialize(String file, String assertion) {
		String str = "";
		String added_from_assertion = "";
		int i = 0;
		
		try {
			FileInputStream fstream = new FileInputStream(file);
			DataInputStream in = new DataInputStream(fstream);
			BufferedReader br = new BufferedReader(new InputStreamReader(in));
			str = null;
			
			// Add sentences to knowledge base one at a time
			while ((str = br.readLine()) != null) {
				KB.add(str);
			}

		} catch (IOException e) {
		}

		// Print out initial knowledge base constants
		System.out.println("Initial KB Contents:");
		while (i < KB.size()) {
			System.out.println(KB.get(i));
			i++;
		}

		// Add negation to assertion to KB
		if (assertion.contains("~")) {
			added_from_assertion = assertion.substring(1);
		}
		else {
			added_from_assertion = "~" + assertion;
		}
		KB.add(added_from_assertion);
		
		System.out.println("Prove assertion: " + assertion);
		System.out.println("Adding " + added_from_assertion + " to the KB");
		System.out.println("START");
		while (!KB.contains(assertion)) {
			runSearch();
		}
		System.out.println("CONTRADICTION: " + added_from_assertion + " & " + assertion);
		System.out.println("Therefore, " + assertion);
		System.out.println("Solution found at search depth: " + depth);
	}
	
	private static void runSearch() {
		boolean stop_single_check = false;
		boolean stop_sentence_check = false;
		int i = 0;
		String sentence = "";
		String resolution = "";
	
		while (i < KB.size() && !stop_single_check) {
			String current = "";
			int j = 0;
			int index = 0;
			
			// Check single characters 
			if (KB.get(i).length() <= 2 && !exhausted.contains(KB.get(i))) {
				current = KB.get(i);
				
				// Check sentences 
				if (current.length() == 1) {
					while (j < KB.size() && !stop_sentence_check) {
						if (KB.get(j).contains("~"+current) && KB.get(j).length() > 2) {
							sentence = KB.get(j);
							index = sentence.indexOf("~" + current);
							
							// Find unit resolution if ~current is at index 0 of sentence
							if (index == 0) {
								resolution = sentence.substring(3);
							}
							else if (index == 3) {
								if (sentence.length()==5) {
									resolution = sentence.substring(0,2);
								}
								else {
									resolution = sentence.substring(0,1);
								}
							}
							
							// If resolution isn't in KB add it and stop current search loop, else continue sentence search
							if (KB.contains(resolution)) {
								j++;
							}
							else {
								stop_sentence_check = true;
								stop_single_check = true;
								KB.add(resolution);
								System.out.println("Add: " + resolution + " (" + sentence + ", " + current + ")");
								exhausted.add(current);
								depth++;
							}
						}
						else {
							if (j == KB.size()-1) {
								exhausted.add(current);
							}
							j++;
						}																								
					}
				}
				else {
					while (j < KB.size() && !stop_sentence_check) {
						if (KB.get(j).contains(current.substring(1)) && KB.get(j).length() > 2 && (KB.get(j).indexOf(current.substring(1))==0 || KB.get(j).charAt(KB.get(j).indexOf(current.substring(1))-1) == 'v')) {
							sentence = KB.get(j);
							index = sentence.indexOf(current.substring(1));
							
							// Find unit resolution if current is at index 0 of sentence
							if (index == 0) {
								resolution = sentence.substring(2);
							}
							else {
								resolution = sentence.substring(0, index-1);
							}
							
							// If resolution isn't in KB add it and stop current search loop, else continue sentence search
							if (KB.contains(resolution)) {
								j++;
							}
							else {
								stop_sentence_check = true;
								stop_single_check = true;
								KB.add(resolution);
								System.out.println("Add: " + resolution + " (" + sentence + ", " + current + ")");
								exhausted.add(current);
								depth++;
							}
						}
						else {
							if (j == KB.size()-1) {
								exhausted.add(current);
							}
							j++;
						}																								
					}
				}
			}
			else {
				if (i == KB.size()-1) {
					i = 0;
					exhausted.clear();
				}
				else {
					i++;
				}
			}
		}
		
	}
}